links2Fifo-impl(es;l1;l2;A;tg)
== <A
== , A
== , {i:Id| (i = source(l1))  (i = destination(l1))} 
== , i,j,e. loc(e) = i & e'@j.((kind(e') = rcv(l1,tg))  (kind(e') = rcv(l2,tg))) & sender(e') = e
== , i,e. loc(e) = i & ((kind(e) = rcv(l1,tg))  (kind(e) = rcv(l2,tg)))
== , i,x,y. x = y
== , > 

latex

---

clarification:

links2Fifo-impl(es;l1;l2;A;tg)
== <A
== , A
== , {i:Id| (i = source(l1)  Id)  (i = destination(l1)  Id)} 
== , i,j,e. es-loc(es; e) = i  Id
== & existse-at(es;
== & existse-at(j;
== & existse-at(e'.(((es-kind(es; e') = rcv(l1,tg)  Knd)  (es-kind(es; e') = rcv(l2,tg)  Knd))
== & existse-at(& es-sender(es; e') = e  es-E(es)))
== , i,e. es-loc(es; e) = i  Id
== & ((es-kind(es; e) = rcv(l1,tg)  Knd)  (es-kind(es; e) = rcv(l2,tg)  Knd))
== , i,x,y. x = y  A
== , > 

latex

Definitions	{x:A| B(x)} , source(l), destination(l), e@i.P(e), E, sender(e), P & Q, Id, loc(e), P  Q, Knd, kind(e), rcv(l,tg), <a, b>, x.A(x), s = t,
FDL editor aliases	links2Fifo-impl